Description Logics (DLs) are a family of knowledge representation formalismsmainly characterised by constructors to build complex concepts and roles fromatomic ones. Expressive role constructors are important in many applications,but can be computationally problematical. We present an algorithm that decidessatisfiability of the DL ALC extended with transitive and inverse roles andfunctional restrictions with respect to general concept inclusion axioms androle hierarchies; early experiments indicate that this algorithm is well-suitedfor implementation. Additionally, we show that ALC extended with justtransitive and inverse roles is still in PSPACE. We investigate the limits ofdecidability for this family of DLs, showing that relaxing the constraintsplaced on the kinds of roles used in number restrictions leads to theundecidability of all inference problems. Finally, we describe a number ofoptimisation techniques that are crucial in obtaining implementations of thedecision procedures, which, despite the worst-case complexity of the problem,exhibit good performance with real-life problems.
展开▼
